
\section{Introduction}\label{sec:introduction}

\levi{\cite{Cicchetti2008,Meyers2011} must appear somewhere.}
Model evolution is implicit during model development. We can consider in fact
that any change to an existing model consists of evolution. For applicability
purposes, in this paper we are interested in evolutions that can be directly
related to a requirement for the software system the model represents. Also,
during this paper we will concentrate on behavioral models. If the model
represents the desired behavior of a software system, then the consequences of a
wrong evolution can be very serious: if the model is to be used as an artifact
by developers, then misunderstandings arising between the modelers and the
developers will lead delays in product delivery; if the model is to be used as
an artifact for model-based testing then false positive of false negatives may
arise in the testing process; if the model is supposed to be used at runtime or
for automatic code synthesis then the wrong product may be delivered to the
costumer. However, not all is bleak -- behavioral models typically have clearly
defined semantics. As this is the case, mathematical and mechanical tools may be
applied to them such that their dynamic properties are verified.

The goal of this paper is to study how a model can safely evolve in a controlled
fashion, in the direction of satisfying the set of requirements stated for the
final software system. In order to do so we will use a specific formalization of
the notions of \emph{model} and \emph{requirement}. We have tried to remain as
generic as possible and have chosen for expressing behavioral models a
fundamental, but usable, computing machine -- algebraic Petri nets (APN) -- and
CTL (Computational Tree Logic) for expressing requirements for those models.

In \Sect\ref{sec:motivation} we describe the confidential file system case study (access control domain, requirements, 3 Statecharts)
In \Sect\ref{sec:operational_dref} we present the formal framework behind our notion of evolution.
In \Sect\ref{sec:prop_preserv_evol} we demonstrate how the each evolved model preserves the features from its earlier version while adding new ones.
Finally, \Sect\ref{sec:related_work} addresses related work and we conclude in \Sect\ref{sec:conclusions}.
